import os
import zlib
from z3 import *

def construct(x, c, a, b):
    for i in range(0, 32):
        if (a >> i)&1 == 1 and (b >> i)&1 == 1:
            x[i] = Xor(x[i], True)
        
        if (a >> i)&1 == 0 and (b >> i)&1 == 1:
            x[i] = Xor(x[i], c)
        
        if (a >> i)&1 == 1 and (b >> i)&1 == 0:
            x[i] = Xor(x[i], Not(c))

def crc(dat):
    return ~zlib.crc32(dat, 0xFFFFFFFF)

a = open("blocks").read()
maxi = len(a)/(0x100)

s = Solver()
ba = []
blocks = []

x = BoolVector('x', 32)
y = BoolVector('y', 32)

for i in range(32):
    x[i] = False
    y[i] = False

c1 = BoolVector("c", maxi)
c2 = BoolVector("d", maxi)

c = [c1,c2]
blocks = []

for i in range(0, maxi):
    ab = [0,0]
    tb = []
    for j in range(0, 2):
        tb.append(a[i*0x100+j*0x80:i*0x100+j*0x80+0x80])
        dat = "\x00"*(i*0x80)+tb[-1]+"\x00"*((maxi-i)*0x80)
        ab[j] = crc(dat)
    ba.append(ab)
    blocks.append(tb)
    
    construct(x, c[0][i], ab[0], ab[1])
    construct(y, c[1][i], ab[0], ab[1])

for i in range(32):
    s.add(x[i] == y[i])

# I know this isn't all of them, I was lazy.
s.add(Or(c[0][0] != c[1][0], c[0][1] != c[1][1], c[0][2] != c[1][2], c[0][3] != c[1][3],
         c[0][8] != c[1][8], c[0][9] != c[1][9], c[0][10] != c[1][10], c[0][11] != c[1][11],
         c[0][12] != c[1][12], c[0][13] != c[1][13], c[0][14] != c[1][14], c[0][15] != c[1][15],
         c[0][4] != c[1][4], c[0][5] != c[1][5], c[0][6] != c[1][6], c[0][7] != c[1][7]))

things = ["", ""]

print "solving"

# 10 minutes z3 you're on
# slim shady only got 6 minutes
s.set("timeout", 1000 * 60 * 10)
if s.check() == sat:
    print "satted"
    m = s.model()
    print m
    x = [0,0]
    for i in range(0, maxi):
        for j in range(0, 2):
            idx = 0
            # wtf man it's late, str()
            if str(m.evaluate(c[j][i])) == "True":
                idx = 1
            things[j] += blocks[i][idx]
            x[j] ^= ba[i][idx]
    
    if things[0] != things[1]:
        print "yay"
    print crc(things[0])
    print crc(things[1])
    print x
    open("out1", "wb").write(things[0])
    open("out2", "wb").write(things[1])
else:
    print "can't sat"
